\begin{tabbing}
ecl{-}machine2($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it upd}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$$z$$\in$update{-}spec{-}vars(${\it upd}$).R{-}state{-}var(\=$i$;${\it ds}$ $\oplus$ $x$ : $T$;${\it da}$;$z$;${\it ds}$($z$);${\it ks}$;\+
\\[0ex]$\lambda$$k$,$s$,$v$,${\it z'}$. list\_accum(\=${\it z'}$,${\it nf}$.\=${\it nf}$/$n$,$f$.\+\+
\\[0ex]if \=$a$($n$,$k$,$s$,$v$,$s$($x$))$\rightarrow$\+
\\[0ex]$f$($s$,$v$)
\-\\[0ex]else ${\it z'}$ fi;
\-\\[0ex]${\it z'}$;
\\[0ex]${\it upd}$($\langle$$k$$,\,$$z$$\rangle$)?nil))
\-\-
\end{tabbing}